1. Field of the Invention
This invention relates generally to the field of verification of circuit designs, and in particular to the visualization of properties used in the verification of a circuit design.
2. Background of the Invention
Over the last 30 years, the complexity of integrated circuits has increased greatly. This increase in complexity has exacerbated the difficulty of verifying circuit designs. In a typical integrated circuit design process, which includes many steps, the verification step consumes approximately 70-80% of the total time and resources. Aspects of the circuit design such as time-to-market and profit margin greatly depend on the verification step. As a result, flaws in the design that are not found during the verification step can have significant economic impact by increasing time-to-market and reducing profit margins. To maximize profit, therefore, the techniques used for verification should be as efficient as possible.
As the complexity in circuit design has increased, there has been a corresponding improvement in various kinds of verification and debugging techniques. In fact, these verification and debugging techniques have evolved from relatively simple transistor circuit-level simulation (in the early 1970s) to logic gate-level simulation (in the late 1980s) to the current art that uses Register Transfer Language (RTL)-level simulation. RTL describes the registers of a computer or digital electronic system and the way in which data are transferred among them.
Existing verification and debugging tools are used in the design flow of a circuit. The design flow begins with the creation of a circuit design at the RTL level using RTL source code. The RTL source code is specified according to a Hardware Description Language (HDL), such as Verilog HDL or VHDL. Circuit designers use high-level hardware description languages because of the size and complexity of modern integrated circuits. Circuit designs are developed in a high-level language using computer-implemented software applications, which enable a user to use text-editing and graphical tools to create a HDL-based design.
In the design flow, creation of the RTL source code is followed by verification of the design to check if the RTL source code meets various design specifications. This verification is sometimes performed by simulation of the RTL code using a “test bench,” which includes stimulus generators and simulation monitors. The verification method involving the use of RTL source code and test bench is referred to as the simulation process. For a circuit having n inputs, there would be 2n possible combinations of inputs at any given time. Where n is large, such as for a complex design, the number of possible input sequences becomes prohibitively large for verification. To simplify the verification process, therefore, only a subset of all possible inputs is described in a particular test bench. Thus, the circuit behavior for all possible combinations of inputs is not checked.
An increasingly popular alternative to simulation is to use formal methods to verify the properties of a design completely. Formal methods use mathematical techniques to prove that a property is either always true or to provide an example condition (called a counterexample) that demonstrates the property is false. Tools that use formal methods to verify RTL source code and design properties are known as “model checkers.” Design properties to be verified include behavior that must be satisfied by the circuit design. Since properties define the design requirements in pure mathematical terms, this enables analysis of all possible valid inputs for a given circuit and is akin to an exhaustive simulation. Formal verification methods are therefore more exhaustive when compared to simulation methods. Moreover, formal verification methods provide many advantages over the simulation methods, such as reduced validation time, quicker time-to-market, reduced costs, and high reliability.
For simulation as well as for formal verification tools, the use of environment and design properties as verification components are becoming more popular recently, typically known as the assertion-based verification (ABV) methodology. Typically ABV requires the user to create a set of properties that can be expressed as temporal sequences of events, accessing primarily the inputs and the internal signals within the design. During the verification process, specific directives, such as “assume,” “assert,” and “cover” are provided for each of these properties. A property that is to be proved or checked is an assertion. A property that is used to constrain the legal values at the inputs of the design during verification is an assumption. To cover a property means using the property as a metric to determine how much of the design has been exercised. Examples of languages for specifying these kinds of verification components include but are not limited to Open Verification Library (OVL), System Verilog Assertion (SVA), and Property Specification Language (PSL).
As users create more complex verification components, this process becomes more onerous. In additional to properties in the form of simple temporal sequences of events, high-level requirements describing the end-to-end behavior of a circuit design in terms of the circuit's input and output signals (e.g., viewing the circuit design from a “black-box” perspective) are also becoming popular. High-level requirements need not be limited to input and output signals, however, and they may also include requirements that describe internal architecture of the design, such as the state of a data path within the design or other internal signals.
The high-level requirements are typically encoded in the requirements model. FIG. 1 illustrates block diagram of a requirements model 120 and a circuit design 130, which are debugged concurrently in accordance with existing verification techniques. The requirements model 120 and the circuit design 130 are coupled so that input signals for the circuit design 130 are also coupled as inputs to the requirements model 120 and the output signals of the circuit design 130 are coupled as inputs to the requirements model 120. In this specific example of a requirement model, the outputs of the requirements model 120, property_0 through property_k, indicate whether particular properties of the set of high-level requirements have been violated.
Regardless of whether simulation or formal verification is used, ensuring the correctness of environment and design properties—whether in the form of assertions, high-level requirements, or other forms—is important for proper verification of a circuit design. Otherwise, errors detected during the verification process may reflect errors in the properties rather than a true error in the circuit design that is being verified.
With traditional simulation and formal verification tools, the related verification components, such as test benches, assertions, or high-level requirements, are debugged at the same time as the design. In one example, a user creates a simulation test bench and then runs a simulation on the design. If the simulation fails, the user checks the test bench and the design. Any problems in the test bench, if responsible for the failure, are fixed to make the simulation pass. In another example, a user writes an assertion and uses a formal verification tool. If the formal verification of the assertion fails, the user checks the assertion and the design. Any problems in the assertion, if responsible for the failure, are fixed to continue the verification process.
When high-level requirements and their requirement model are debugged along with the circuit design during the formal verification process, the complexity of the debugging effort is further increased. In the extreme, these requirements may be a self-contained, high-level model that can be simulated, such as a process model implementing an instruction set architecture or a SystemC transaction-based model of the design. While in some cases the requirements can be simulated with simulation vectors to determine their correctness, it is generally difficult to create simulation vectors to simulate assertions or requirements that do not represent a self-contained, high-level model of the design.
Such a concurrent verification scheme of debugging the design and the verification components at the same time leads to inefficiencies in the debugging and verification processes. In the example explained above, a detected violation of a design may be due either to a bug in the circuit design 130 or in the way in which the requirement model 120 is expressed. Accordingly, it is desirable to improve upon existing verification methodologies to avoid such inefficiencies and uncertain results.